es:ES{i}, C, R:Type{i}, F:((C List)R), I:AbsInterface(C), O:AbsInterface(R).
state-machine-spec{i:l}(es; C; R; F; I; O)  {i'} 

latex

Definitions

t  T, True, T, x:A. B(x), P  Q, b, x:AB(x), SqStable(P), {x:A| B(x)} , E(X), f(a), EState(T), Id, , pred!(e;e'), SWellFounded(R(x;y)), loc(e), <a, b>, s = t, A, constant_function(f;A;B), Type, kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x:A  B(x), P & Q, Top, , e < e', r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Unit, left + right, Msg(M), type List, IdLnk, EOrderAxioms(E; pred?; info), EqDecider(T), ES, AbsInterface(A), P  Q, retrace(es; Q; X), g glues Ia:Qa f Ib:Rb, Q-R-glued(es; Ib_valtype; f; Ia; Qa; Ib; Rb), [], [car / cdr], let x,y = A in B(x;y), t.1, E, Void, x:A.B(x), x:A. B(x), retracer(p), as @ bs, X(e), x.A(x), map(f;as), (e <loc e'), A c B, , P  Q, (x  l), x before y  l, state-machine-spec{i:l}(es; C; R; F; I; O)

Lemmas

retrace wf, es-locl wf, Q-R-glued wf, map wf, es-interface-val wf, append wf, retracer wf, subtype rel function, subtype rel sum, es-E-interface wf, val-axiom wf, constant function wf, sq stable from decidable, decidable assert